deferred val +' : (int * int) -> int
where (forall (x, y). pre ( +') (x, y))
  and (forall (x, y, z). post ( +' ) (x, y) (z) <=> z = x + y)
let f (x) = 
  let logic y = x in
  let logic y = y + 1 in
  let z = x +' 1 in
    assert (y = z) in 
    z
